Nuprl Definition : Kind-deq
0,22
postcript
pdf
KindDeq == union-deq(IdLnk
Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
latex
Definitions
union-deq(
A
;
B
;
a
;
b
)
,
product-deq(
A
;
B
;
a
;
b
)
,
IdLnk
,
Id
,
IdLnkDeq
,
IdDeq
FDL editor aliases
Kind-deq
origin
Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)